(* The module for translation between boolean programs and boolean flow graphs *)

open Ast;;
open Datatypes;;

exception Illegal_cn of string;;

(*** For numbering and creating control nodes. Control nodes = Controlnode(Int) and is denoted cn *)

let nodeNum = ref 0;;
let createCN () = nodeNum := (!nodeNum + 1); ControlNode(!nodeNum);;
let undoCN () = nodeNum := (!nodeNum - 1); ();;

(*** END ************)


(*** Functions to handle variables list. ***)

(* Removes the variable var from the list varList *)
let removeVar var varList = List.filter (fun var1 -> var <> var1) varList;;

(* Removes all the variables in the first list from the second list *)
let removeVars varList1 varList2 = List.filter (fun var -> not (List.mem var varList1)) varList2;;

(* Determines if the variable (var) is contained in the variable list (varList) *)
let varIsIn var varList = List.mem var varList;;

(*** END ************)


(*** Functions to get variables lists, list containing strings (the names of the variables). ***)

(* Gets the names of the declared variables in a declaration block *)
let getDeclaredVars decl = 
  let rec getDeclaredVar varList = function
    Declaration(_, var) -> var :: varList
    | Declcomp(_, decl1, decl2) -> let varList1 = getDeclaredVar varList decl1 in getDeclaredVar varList1 decl2
    | _ -> varList
  in
    getDeclaredVar [] decl
  ;;

(* Gets the names of the real global variables in a Boolean program *)
let getGlobals bp = let Bp(decl, _) = bp in getDeclaredVars decl;; (* ret is a reserved global variable *)
  
(* Gets the names of the formal parameters in a procedure *)
let getFormalParameters (Procedure(_, _, _, fp, _, _)) = fp;;

(* Gets the names of the local variables in a procedure *)
let getLocals (Procedure(_, _, _, _, d, _)) = getDeclaredVars d;;

(* Gets the names of the global variables in a procedure given a set of real globals, this is a subset (not strict) of the real globals *)
let getGlobalsInProc glob proc = 
  let glob1 = removeVars (getFormalParameters proc) glob in
    removeVars (getLocals proc) glob1
  ;;

(*** END ************)


(*** Functions to get variables lists, list containing strings (the names of the variables). ***)

(* Gets pre-label of Statement *)
let getPreLabelOfStm = function 
	Skip(Labels(pre, post)) -> pre
	| Comp(Labels(pre, post), _, _) -> pre
	| Callvoid(Labels(pre, post), _, _) -> pre
	| Callbool(Labels(pre, post), _, _, _) -> pre
	| Assignment(Labels(pre, post), _, _) -> pre
	| While(Labels(pre, post), _, _) -> pre
	| Returnvoid(Labels(pre, post)) -> pre
	| Returnbool(Labels(pre, post), _) -> pre
	| Ifelse(Labels(pre, post), _, _, _) -> pre
	;;

(* Gets start-label of a procedure, i.e. the first pre-label not belonging to the procedure itself or a compound *)
let getStartLabelOfProc procedure = 
	let Procedure(_, _, _, _, d, s) = procedure in
		match d with
			Declaration(Labels(pre,post), _) -> pre
			| Declcomp(Labels(pre, post), _, _) -> pre
			| _ -> getPreLabelOfStm s
			;;

(*** END ************)
      

(*** Functions to handle control node triples (and wrapped control node triples), denoted cnTriples. A cnTriple is a triple (cn, label, state). This is our "configurations" in the execution. A wrapped cnTriple, denoted WCNTriple, is a cnTriple wrapped in as Visited(cnTriple) or Unvisited(cnTriple) ***)

(* Compares two cnTriples for equality against a label map. *)
let compareCNTriples labMap (cn1, label1, state1) (cn2, label2, state2) =
  if (((Locations.getLocation label1 labMap) = (Locations.getLocation label2 labMap)) && (state1 = state2)) then
    true
  else
    false
  ;;
  
(* Given a list of visited cnTriples and a cnTriple this returns an equal cnTriple in the list if it exist or None otherwise *)
let getIfVisited labMap cnTriple visitedCNTriples = 
    try Some(List.find (compareCNTriples labMap cnTriple) visitedCNTriples) with
      Not_found -> None
    ;;

(* creates a WCNTriple given a label map, a label and a state *)    
let createWCNTriple visitedCNTriples labMap label state =
  let cn = createCN () in
    match getIfVisited labMap (cn, label, state) visitedCNTriples with
      Some(vCN, vLabel, vState) -> undoCN (); Visited(vCN, vLabel, vState) (* we "give back" the cn-numbering *)
      | None -> Unvisited(cn, label, state)
    ;;

(* creates a list of WCNTriple given a label map, a label and a list of states. One WCNTriple for each state *)
let createWCNTriples visitedCNTriples labMap label states = 
	let rec addCN cns = function (* match states *)
		state :: rest -> addCN ((createWCNTriple visitedCNTriples labMap label state) :: cns) rest (* must set the return value save it *)
		| [] -> cns
	in
		addCN [] states
	;;
  
(* Gets the control node of a wrapped cnTriple *)
let getTCN = function
  (Visited(cn, _, _) | Unvisited(cn, _, _)) -> cn;;
 
(* Gets the state of a wrapped cnTriple *) 
let getTState = function
  (Visited(_, _, state) | Unvisited(_, _, state)) -> state;;
  
(* Gets a list of entrytriples, i.e. WCNTriples where the procedure are allowed to start execute, for a procedure, given a set of real globals, a procedure and a label map. *)
let createEntryNodes labMap proc glob = 
  let varInEntry = (glob @ (getFormalParameters proc)) in
	let entryStates = States.allValuations varInEntry in
	let startLabel = getStartLabelOfProc proc in
    if (List.length entryStates > 0) then
      List.map (createWCNTriple [] labMap startLabel) entryStates (* or rev_map, tail recursive *)
    else
      [createWCNTriple [] labMap startLabel []]
  ;;

(*** END ************)		
		
    
    
    
(*the transitions *) 

(* create a map from locations to code = dec/stm *)
let rec createLocToCodeMapDec labMap map decl = 
	match decl with
		Declaration(Labels(pre, _), _) -> 
			let loc = Locations.getLocation pre labMap in
				(loc, CodeDecl(decl)) :: map
		| Declcomp(_, decl1, decl2) -> 
			let map1 = createLocToCodeMapDec labMap map decl1 in
				createLocToCodeMapDec labMap map1 decl2
		| _ -> map
		;;

let rec createLocToCodeMapStm labMap map stm =
	match stm with
		Comp(_, stm1, stm2) -> 
			let map1 = createLocToCodeMapStm labMap map stm1 in
				createLocToCodeMapStm labMap map1 stm2
		| ( Skip(Labels(pre, _)) | Callvoid(Labels(pre, _), _, _) | Callbool(Labels(pre, _), _, _, _) | Assignment(Labels(pre, _), _, _) | Returnvoid(Labels(pre, _)) | Returnbool(Labels(pre, _), _) ) ->
			let loc = Locations.getLocation pre labMap in
				(loc, CodeStm(stm)) :: map
		| While(Labels(pre, _), _, stm1) ->
			let map1 = createLocToCodeMapStm labMap map stm1 in
			let loc = Locations.getLocation pre labMap in
				(loc, CodeStm(stm)) :: map1
		| Ifelse(Labels(pre, _), _, stm1, stm2) ->
			let map1 = createLocToCodeMapStm labMap map stm1 in
			let map2 = createLocToCodeMapStm labMap map1 stm2 in
			let loc = Locations.getLocation pre labMap in
				(loc, CodeStm(stm)) :: map2
	;;
	
let createLocToCodeMap labMap proc =
	let Procedure(_, _, _, _, d, s) = proc in
	let map1 = createLocToCodeMapDec labMap [] d in
		createLocToCodeMapStm labMap map1 s
	;;
	

(* help to createTransition, returns a list of triples (cn, string (a label), cn) *)
let createTransitions cn labelStr cnTripleList = 
	let rec addTrans transitions = function (* match states *)
		Unvisited(nextCN, _, _) :: rest -> addTrans ((cn, labelStr, nextCN) :: transitions) rest
    | Visited(nextCN, _, _) :: rest -> addTrans ((cn, labelStr, nextCN) :: transitions) rest
		| [] -> transitions
	in
		addTrans [] cnTripleList
	;;
		

let getCodeFromLoc loc locToCMap = 
	try List.assoc loc locToCMap with
		Not_found -> Nothing
	;;

(* create a valuation map for the control node cn, with the extra "variables" in extraList *)
let createValuation cn extraList state = Some((cn, extraList @ (States.trueVarList state)));;

let addValuation valuation valuationList =
  match valuation with
    Some(v) -> v :: valuationList
    | None -> valuationList
  ;;
   
(* returns a set of transitions [(node, label, node)], a valuation map [(node, [string])] and a set of cntriples*)
let createAll pName glob returnCNs visitedCNTriples locToCMap labMap cnTriple =
  match cnTriple with
  Visited(_, _, _) -> ([], None, [], glob, returnCNs, visitedCNTriples)
  | Unvisited(cn, label, state) ->
  begin
	if (List.mem cn returnCNs) then (* if the current control node is a marked as a return node *)
		([], createValuation cn [pName; "r"] state, [], glob, returnCNs, visitedCNTriples) (* no transitions, valuation with r+, no more CNTriples, glob same, same return nodes *)
	else begin
    let fromState = 
      if States.containsVar state "ret" then
        States.removeVar state "ret"
      else
        state
    in
		let code = getCodeFromLoc (Locations.getLocation label labMap) locToCMap in
			match code with
				CodeStm(Skip(Labels(_, post))) -> 
					let nextCNTriple = createWCNTriple visitedCNTriples labMap post fromState in
						(createTransitions cn "eps" [nextCNTriple], createValuation cn [pName] state, [nextCNTriple], glob, returnCNs, visitedCNTriples)
				| CodeStm(Callvoid(Labels(_, post), id, expList)) ->
					let nextStates = States.allValuationsFromState fromState glob in
					let nextCNTriples = createWCNTriples visitedCNTriples labMap post nextStates in
					let labelString = id ^ "(" ^ (Evaluate.stringFromExpList state expList) ^ ")" in
					let transitions = createTransitions cn labelString nextCNTriples in
						(transitions, createValuation cn [pName] state, nextCNTriples, glob, returnCNs, visitedCNTriples)
				| CodeStm(Callbool(Labels(_, post), var, id, expList)) ->
					let nextStates = States.allValuationsFromState fromState ("ret" :: (removeVar var glob)) in
					let assignedNextStates = (* assign var the value of ret, the return value *)
						List.map 
							(fun stateToChange -> States.setVar stateToChange var (States.getValue stateToChange "ret")) 
							nextStates 
					in
					let nextCNTriples = createWCNTriples visitedCNTriples labMap post assignedNextStates in
					let labelString = id ^ "(" ^ (Evaluate.stringFromExpList state expList) ^ ")" in
					let transitions = createTransitions cn labelString nextCNTriples in
						(transitions, createValuation cn [pName] state, nextCNTriples, glob, returnCNs, visitedCNTriples)
				| CodeStm(Assignment(Labels(_, post), varList, exprList)) ->
					let valueList = Evaluate.evaluateList state exprList in
					let nextState = States.setVars fromState varList valueList in
					let nextCNTriple = createWCNTriple visitedCNTriples labMap post nextState in
						(createTransitions cn "eps" [nextCNTriple], createValuation cn [pName] state, [nextCNTriple], glob, returnCNs, visitedCNTriples)
				| CodeStm(While(Labels(_, post), decider, s)) ->
					let nextCNTriples = 
          match decider with
            Expression(exp) ->
              if ((Evaluate.evaluate state exp) = False) then
                [(createWCNTriple visitedCNTriples labMap post fromState)]
              else
                [(createWCNTriple visitedCNTriples labMap (getPreLabelOfStm s) fromState)]
            | Undet -> 
              let nextCNTriple1 = (createWCNTriple visitedCNTriples labMap post fromState) in
              let nextCNTriple2 = (createWCNTriple visitedCNTriples labMap (getPreLabelOfStm s) fromState) in
                [nextCNTriple1;  nextCNTriple2]
					in
						(createTransitions cn "eps" nextCNTriples, createValuation cn [pName] state, nextCNTriples, glob, returnCNs, (cn, label, fromState) :: visitedCNTriples) (* While is the only statement we can loop with, thus we only need to add the cn for while to the visitedCNs list *)
				| CodeStm(Ifelse(Labels(_, post), decider, s1, s2)) ->
					let nextCNTriples = 
          match decider with
            Expression(expr) ->
              if ((Evaluate.evaluate state expr) = False) then
                [(createWCNTriple visitedCNTriples labMap (getPreLabelOfStm s2) fromState)]
              else
                [(createWCNTriple visitedCNTriples labMap (getPreLabelOfStm s1) fromState)]
            | Undet ->
              let nextCNTriple1 = (createWCNTriple visitedCNTriples labMap (getPreLabelOfStm s2) fromState) in
              let nextCNTriple2 = (createWCNTriple visitedCNTriples labMap (getPreLabelOfStm s1) fromState) in
                [nextCNTriple1; nextCNTriple2]
					in
						(createTransitions cn "eps" nextCNTriples, createValuation cn [pName] state, nextCNTriples, glob, returnCNs, visitedCNTriples)
				| CodeStm(Returnvoid(Labels(_, post))) ->
					let nextCNTriple = createWCNTriple visitedCNTriples labMap post fromState in
						(createTransitions cn "eps" [nextCNTriple], createValuation cn [pName] state, [nextCNTriple], glob, ((getTCN nextCNTriple) :: returnCNs), visitedCNTriples)
				| CodeStm(Returnbool(Labels(_, post), expr)) ->
          let nextState = States.declareVar fromState "ret" in
					let nextState = States.setVar nextState "ret" (Evaluate.evaluate state expr) in
					let nextCNTriple = createWCNTriple visitedCNTriples labMap post nextState in
						(createTransitions cn "eps" [nextCNTriple], createValuation cn [pName] state, [nextCNTriple], glob, ((getTCN nextCNTriple) :: returnCNs), visitedCNTriples)
				| CodeDecl(Declaration(Labels(_, post), var)) ->
					let nextCNTriple = createWCNTriple visitedCNTriples labMap post (States.declareVar fromState var) in
						(createTransitions cn "eps" [nextCNTriple], createValuation cn [pName] state, [nextCNTriple], removeVar var glob, returnCNs, visitedCNTriples)
				| Nothing -> ([], None, [], glob, returnCNs, visitedCNTriples)
        | _ -> ([], None, [], glob, returnCNs, visitedCNTriples) (* this is spurious, the code will never be comp or declcomp *)
	end
  end
	;;
			
let createTVPair pName glob locToCMap labMap cnTripleStack = 
	let rec iterateCNTriples glob returnCNs visitedCNTriples trans valuations cnTripleStack =
		match cnTripleStack with
		cnTriple :: rest -> 
			let (transitions, valuation, nextCNTriples, newGlob, newReturnCNs, newVisitedCNTriples) = createAll pName glob returnCNs visitedCNTriples locToCMap labMap cnTriple in 
						iterateCNTriples newGlob newReturnCNs newVisitedCNTriples (transitions @ trans) (addValuation valuation valuations) (nextCNTriples @ rest)
		| [] -> (trans, valuations)
	in
		iterateCNTriples glob [] [] [] [] cnTripleStack
	;;	